$\forall$$T$:Type, $L$, $L_{1}$, $L_{2}$:$T$ List. interleaving($T$;$L_{1}$;$L_{2}$;$L$) $\Rightarrow$ $\parallel$$L$$\parallel$ $=$ $\parallel$$L_{1}$$\parallel$+$\parallel$$L_{2}$$\parallel$ $\in$ $\mathbb{N}$